Nuprl Lemma : normal-ds-single 0,22

x:Id, T:Type. Normal(T Normal(x : T
latex


DefinitionsType, Normal(ds), xdom(f). v=f(x  P(x;v), Normal(T), f(x), b, x  dom(f), x : v, xt(x), x.A(x), P  Q, P & Q, x:AB(x), x:AB(x), IdDeq, Top, x:AB(x), Void, Atom$n, s ~ t, Prop, s = t, Id, SQType(T), x:AB(x), P  Q, {T}, t  T
LemmasId sq, Id wf, id-deq wf, fpf-single-dom, top wf, fpf-single wf, fpf-dom wf, assert wf, normal-type wf

origin